T:Type, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}), A:es_realizer{i:l}.
R-compat{i:l}(Rall(L; x.R(x)); A)  (x:T. (x  L)  R-compat{i:l}(R(x); A)) 

latex

Definitions	prop{i:l}, x. t(x), P  Q, P  Q, t  T, P  Q, x(s), P  Q, x:A. B(x)
Lemmas	es realizer wf, R-compat wf, l member wf, Rall wf, R-compat-symmetry, R-compat-Rall